\documentclass{article}
\usepackage{url}
\usepackage{fullpage}
\usepackage{proof}
\usepackage{amssymb}
\usepackage{latexsym}
\usepackage{xcolor}
\usepackage{amsmath, amsthm}

\newcommand{\frank}[1]{\textcolor{blue}{\textbf{[#1 --Frank]}}}
% My own macros
\newcommand{\m}[3]{ \{#1_1 \mapsto #2_1, ... , #1_n \mapsto #2_n\}#3} 
\newtheorem{definition}{Definition}
\newtheorem{lemma}{Lemma}
\newtheorem{theorem}{Theorem}

\begin{document}
%\pagestyle{empty}
\title{Lambda Calculus and Programming}
\author{Peng Fu}
\date{\today}


\maketitle
\thispagestyle{empty}

\section{Definition}
\begin{definition}[Expression]

Expression live in sense world. 
\noindent $ t \ ::= \ x \ | \ t t' \ | \ \lambda x.t $.

\end{definition}

\begin{definition}[Objects]
Objects live in metaphisical world, consists of data(numerals, strings, expressions), functions, structures, programs. 
\end{definition}

Metaphisical world contains sense world. Expression can directly go into metaphisical world. But
metaphisical object can only be talked about in the sense world. Namely, one can associate(using meta language) metaphisical object to an expression. 
\begin{definition}[Meta Language]

Meta language is used to associate objects to expressions, manipulate expressions(namely, beta-reduction, simplification, dereference). So it really is what we call programming language.   
  
\end{definition}





\end{document}
